Early discussion of what came to be known as homotopy type theory:
Proof that every simplicial model category in which the cofibrations are monomorphisms provides a sound model for intensional Martin-Löf type theory (i.e. including the identity types used in homotopy type theory):
On the categorical semantics of dependent type theory via comprehension categories:
Last revised on February 15, 2023 at 06:59:02. See the history of this page for a list of all contributions to it.